\documentclass[a4paper,10pt]{article}
\usepackage[utf8]{inputenc}
\usepackage{amssymb,amsmath}
\usepackage{graphicx}
\usepackage[linesnumbered]{algorithm2e}
\usepackage{float}
\usepackage[brazil]{babel}



\mathchardef\mhyphen="2D

\title{MAC5789\\
Laboratório de Inteligência Artificial\\
Projeto 2 - Revisão de Crenças\\
Profa. Renata Wassermann}
\author{Renato Urquiza Lundberg}

\begin{document}

\maketitle


\pagebreak

\section{Introdução}

Este relatório descreve o processo de realização dos experimentos propostos
como segundo projeto da disciplina de Laboratório de Inteligência Artificial,
e seus resultados.

O projeto consiste na criação de um sistema capaz de identificar, dados um
conjunto de cláusulas satisfatível $B$ e uma cláusula $\alpha$ que pode ser
deduzida a partir da base, um subconjunto maximal do conjunto de cláusulas tal
que não seja possível deduzir a sentença. Este subconjunto é um dos elementos 
de um remainder set, portanto o algoritmo para encontrar este grupo é primordial
 para operações sobre bases de crenças.

Uma vez que tal sistema tenha sido construído, devem ser elaborados diversos
experimentos que avaliem o impacto de diversas variáveis que caracterizam
instâncias do problema na dificuldade em resolvê-lo. Devem ser variados o 
número de variáveis, o número de cláusulas, o tamanho de $\alpha$ e o tamanho
máximo das cláusulas.

\pagebreak

\section{Desenvolvimento}

Este projeto teve relativamente pouco desenvolvimento, pois grande parte de
suas funcionalidades já haviam sido implementadas em outros projetos, que foram
feitos com cuidado para proporcionar modularidade e reutilização de código,
além de possuirem testes detalhados que garantem que cada trecho funciona
de forma independente e correta.

Como o projeto sendo realizado para minha tese trata justamente de algoritmos
para revisão de crenças, foi muito natural utilizar parte de seu código para
este projeto. Este originalmente utilizava o Sat4j como resolvedor, mas foi
adaptado para utilizar a integração com o MiniSAT implementada no projeto 1
desta disciplina.

Tendo como base o gerador de casos de teste proposicionais também feito para
o projeto 1, foi desenvolvido um conjunto de geradores para que fosse possível
gerar conjuntos de cláusulas arbitrárias e de horn, cláusulas isoladas e casos
para contração, constituídos de uma base satisfatível $B$ e uma sentença
$\alpha$ contida no fecho lógico de $B$.

Como em todos os projetos foi mantida um bom isolamento de cada componente, será
possível reutilizar futuramente a integração com o MiniSAT e o gerador de casos
de teste.

\pagebreak

\section{Experimentos}

\subsection{Medições}

Cada cenário é criado de forma aleatória tendo os seguintes parâmetros: tipo
de cláusula (arbitrária ou de Horn), número de variáveis, número de cláusulas,
tamanho de $\alpha$, tamanho mínimo das cláusulas e tamanho máximo das
cláusulas.

Para avaliar a influência de cada variável independentemente, foram feitas
diversas medidas em dezenas de cenários criados utilizando os parâmetros,
variando independentemente cada uma. Para cada configuração foram criados 50
cenários com cláusulas arbitrárias e 50 cenários com cláusulas de Horn.

Foram medidos os valores médios para o tempo total gasto, tempo gasto com o SAT
Solver, número de chamadas ao SAT Solver e tempo gasto por chamada. Para
cada variável será apresentado um gráfico representando a variação destes
valores em função da variação em cada uma, com uma série para cláusulas
arbitrárias e outra para cláusulas de Horn.

\subsection{Número de variáveis}

O número de variáveis foi testado para valores entre 20 e 39, com $B$ com
100 cláusulas com tamanho entre 5 e 10 literais e um $\alpha$ de tamanho 10.

O tempo de execução se manteve quase estável com relação ao número
de variáveis. O tempo de execução com cláusulas de Horn tendeu a ser
ligeiramente menor.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nVariables/tempoExecucao.png}
\end{center}
\end{figure}

O tempo gasto com o SAT Solver evidencia que praticamente todo o tempo
gasto pelo algoritmo é consumido pelas chamadas ao solver.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nVariables/tempoSolver.png}
\end{center}
\end{figure}

O número de chamadas ao solver se manteve quase estável ao longo
destes experimentos, com algumas variações mas nada muito relevante.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nVariables/chamadas.png}
\end{center}
\end{figure}

O tempo gasto por chamada ao solver se manteve praticamente constante,
com exeção do tempo gasto com 20 variáveis, que foi sutilmente maior,
e com o tempo gasto com cláusulas de Horn com 21 variáveis, que
foi ligeiramente maior.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nVariables/tempoPorChamada.png}
\end{center}
\end{figure}

\pagebreak

\subsection{Número de cláusulas}

O número de cláusulas foi testado para valores entre 60 e 99, com $B$ com
20 variáveis e cláusulas com tamanho entre 5 e 10 literais e um $\alpha$ de
tamanho 10.

O aumento do número de cláusulas em $B$, ao contrário do número de variáveis
, gerou uma nítida tendência de aumento no tempo de execução.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nClauses/tempoExecucao.png}
\end{center}
\end{figure}

Mais uma vez, o tempo gasto pelo solver é praticamente todo o tempo gasto pelo
algoritmo, confirmando a baixa sobrecarga.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nClauses/tempoSolver.png}
\end{center}
\end{figure}

O número de chamadas ao solver também teve um aumento nítido, e claramente o
número de chamadas é fortemente relacionado ao tempo de execução do algoritmo.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nClauses/chamadas.png}
\end{center}
\end{figure}

O tempo por chamada teve um aparente crescimento entre 60 e 85 variáveis,
voltando a ter uma tendência de descida de 95 em diante.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{nClauses/tempoPorChamada.png}
\end{center}
\end{figure}

\pagebreak

\subsection{Tamanho de $\alpha$}

O tamanho de $\alpha$ foi testado para valores entre 10 e 14, o número de
variáveis foi fixo em 25 em bases com 100 cláusulas  com tamanho entre 5 e 10
literais.

Não houve diferença expressiva no tempo de execução entre cláusulas arbitrárias
e cláusulas de Horn. O tempo com cláusulas de Horn parece ser ligeiramente
melhor para $\alpha$ com tamanho entre 11 e 13, piorando para tamanhos menores
ou maiores.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{alphaSize/tempoExecucao.png}
\end{center}
\end{figure}

Outra o solver consumiu praticamente todo o tempo do algoritmo.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{alphaSize/tempoSolver.png}
\end{center}
\end{figure}

O número de chamadas seguiu o tempo de execução, o número de chamadas ao solver
para cláusulas de Horn se mostrou ligeiramente menor para $\alpha$ entre 11
e 13.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{alphaSize/chamadas.png}
\end{center}
\end{figure}

O tempo por chamada mostrou ter uma tendência decrescente para $alpha$ com
tamanho a partir de 11, mas a queda no tempo foi mais acentuada para cláusulas
arbitrárias.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{alphaSize/tempoPorChamada.png}
\end{center}
\end{figure}

\pagebreak

\subsection{Tamanho máximo das cláusulas}

O tamanho máximo das cláusulas andou juntamente com o tamanho mínimo, nos testes
realizados. Foram testadas bases de conhecimento com cláusulas de 5 a 10, 6 a
11, 7 a 12, 8 a 13 e de 9 a 14. Para todos os testes foram utilizadas 25
variáveis e 100 cláusulas e $\alpha$ de tamanho 15.

O tamanho máximo das cláusulas provocou uma clara tendência de aumento no tempo
de execução, apesar do tempo com cláusulas de Horn ter sido um pouco menor
com cláusulas de 7 a 12 e o tempo com cláusulas arbitrárias ter apresentado
uma queda para cláusulas de 8 a 13.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{clauseSize/tempoExecucao.png}
\end{center}
\end{figure}

Mais uma vez o tempo é dominado pelas chamadas ao solver.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{clauseSize/tempoSolver.png}
\end{center}
\end{figure}

O número de chamadas ao solver acompanha de perto a tendência do tempo de
execução.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{clauseSize/chamadas.png}
\end{center}
\end{figure}

O tempo por chamada ao solver possui uma tendência exclusivamente crescente
para os testes com cláusulas de Horn, enquanto para cláusulas arbitrárias
foi observada uma pequena queda para cláusulas de tamanho maior.

\begin{figure}[H]
\begin{center}
 \includegraphics[scale=0.5]{clauseSize/tempoPorChamada.png}
\end{center}
\end{figure}

\pagebreak

\section{Conclusão}

Infelizmente os testes realizados não foram suficientes para gerar resultados
conclusivos.

O número de cenários por parâmetro foi relativamente baixo, o que
gera grande incerteza nos resultados.

O tamanho dos cenários também não colaborou, o tempo médio para cada chamada
ao solver ficou em torno de 1 milésimo de segundo, uma escala em que a
sobrecarga da chamada, representa grande parte do tempo da chamada. Com isso a
medida da ``complexidade'' do problema fica prejudicada.

Ficou evidente que a geração de cenários não pode ser feita no momento em que
os testes são realizados, e sim criados com antecedência. O processo de
elaboração dos cenários funciona na base da tentativa e erro, pois nem todo
cenário aleatório atende aos requisitos, tomando um tempo muito maior que o
próprio algoritmo que se quer testar. Em um próximo experimento, certamente
deverá ser considerada a criação de um conjunto grande de cenários de testes
para só então serem realizados os experimentos.

\end{document}